↳ Prolog
↳ PrologToPiTRSProof
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
REM_IN_GGA(X, Y, R) → U1_GGA(X, Y, R, notZero_in_g(Y))
REM_IN_GGA(X, Y, R) → NOTZERO_IN_G(Y)
U1_GGA(X, Y, R, notZero_out_g(Y)) → U2_GGA(X, Y, R, sub_in_gga(X, Y, Z))
U1_GGA(X, Y, R, notZero_out_g(Y)) → SUB_IN_GGA(X, Y, Z)
SUB_IN_GGA(s(X), s(Y), Z) → U6_GGA(X, Y, Z, sub_in_gga(X, Y, Z))
SUB_IN_GGA(s(X), s(Y), Z) → SUB_IN_GGA(X, Y, Z)
U2_GGA(X, Y, R, sub_out_gga(X, Y, Z)) → U3_GGA(X, Y, R, rem_in_gga(Z, Y, R))
U2_GGA(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGA(Z, Y, R)
REM_IN_GGA(X, Y, X) → U4_GGA(X, Y, notZero_in_g(Y))
REM_IN_GGA(X, Y, X) → NOTZERO_IN_G(Y)
U4_GGA(X, Y, notZero_out_g(Y)) → U5_GGA(X, Y, geq_in_gg(X, Y))
U4_GGA(X, Y, notZero_out_g(Y)) → GEQ_IN_GG(X, Y)
GEQ_IN_GG(s(X), s(Y)) → U7_GG(X, Y, geq_in_gg(X, Y))
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
REM_IN_GGA(X, Y, R) → U1_GGA(X, Y, R, notZero_in_g(Y))
REM_IN_GGA(X, Y, R) → NOTZERO_IN_G(Y)
U1_GGA(X, Y, R, notZero_out_g(Y)) → U2_GGA(X, Y, R, sub_in_gga(X, Y, Z))
U1_GGA(X, Y, R, notZero_out_g(Y)) → SUB_IN_GGA(X, Y, Z)
SUB_IN_GGA(s(X), s(Y), Z) → U6_GGA(X, Y, Z, sub_in_gga(X, Y, Z))
SUB_IN_GGA(s(X), s(Y), Z) → SUB_IN_GGA(X, Y, Z)
U2_GGA(X, Y, R, sub_out_gga(X, Y, Z)) → U3_GGA(X, Y, R, rem_in_gga(Z, Y, R))
U2_GGA(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGA(Z, Y, R)
REM_IN_GGA(X, Y, X) → U4_GGA(X, Y, notZero_in_g(Y))
REM_IN_GGA(X, Y, X) → NOTZERO_IN_G(Y)
U4_GGA(X, Y, notZero_out_g(Y)) → U5_GGA(X, Y, geq_in_gg(X, Y))
U4_GGA(X, Y, notZero_out_g(Y)) → GEQ_IN_GG(X, Y)
GEQ_IN_GG(s(X), s(Y)) → U7_GG(X, Y, geq_in_gg(X, Y))
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
↳ PiDP
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
From the DPs we obtained the following set of size-change graphs:
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
SUB_IN_GGA(s(X), s(Y), Z) → SUB_IN_GGA(X, Y, Z)
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
SUB_IN_GGA(s(X), s(Y), Z) → SUB_IN_GGA(X, Y, Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
SUB_IN_GGA(s(X), s(Y)) → SUB_IN_GGA(X, Y)
From the DPs we obtained the following set of size-change graphs:
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
REM_IN_GGA(X, Y, R) → U1_GGA(X, Y, R, notZero_in_g(Y))
U2_GGA(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGA(Z, Y, R)
U1_GGA(X, Y, R, notZero_out_g(Y)) → U2_GGA(X, Y, R, sub_in_gga(X, Y, Z))
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
REM_IN_GGA(X, Y, R) → U1_GGA(X, Y, R, notZero_in_g(Y))
U2_GGA(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGA(Z, Y, R)
U1_GGA(X, Y, R, notZero_out_g(Y)) → U2_GGA(X, Y, R, sub_in_gga(X, Y, Z))
notZero_in_g(s(X)) → notZero_out_g(s(X))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
U2_GGA(Y, sub_out_gga(Z)) → REM_IN_GGA(Z, Y)
REM_IN_GGA(X, Y) → U1_GGA(X, Y, notZero_in_g(Y))
U1_GGA(X, Y, notZero_out_g) → U2_GGA(Y, sub_in_gga(X, Y))
notZero_in_g(s(X)) → notZero_out_g
sub_in_gga(s(X), s(Y)) → U6_gga(sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X)
U6_gga(sub_out_gga(Z)) → sub_out_gga(Z)
notZero_in_g(x0)
sub_in_gga(x0, x1)
U6_gga(x0)
REM_IN_GGA(y0, s(x0)) → U1_GGA(y0, s(x0), notZero_out_g)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
U2_GGA(Y, sub_out_gga(Z)) → REM_IN_GGA(Z, Y)
REM_IN_GGA(y0, s(x0)) → U1_GGA(y0, s(x0), notZero_out_g)
U1_GGA(X, Y, notZero_out_g) → U2_GGA(Y, sub_in_gga(X, Y))
notZero_in_g(s(X)) → notZero_out_g
sub_in_gga(s(X), s(Y)) → U6_gga(sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X)
U6_gga(sub_out_gga(Z)) → sub_out_gga(Z)
notZero_in_g(x0)
sub_in_gga(x0, x1)
U6_gga(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
U2_GGA(Y, sub_out_gga(Z)) → REM_IN_GGA(Z, Y)
REM_IN_GGA(y0, s(x0)) → U1_GGA(y0, s(x0), notZero_out_g)
U1_GGA(X, Y, notZero_out_g) → U2_GGA(Y, sub_in_gga(X, Y))
sub_in_gga(s(X), s(Y)) → U6_gga(sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X)
U6_gga(sub_out_gga(Z)) → sub_out_gga(Z)
notZero_in_g(x0)
sub_in_gga(x0, x1)
U6_gga(x0)
notZero_in_g(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
U2_GGA(Y, sub_out_gga(Z)) → REM_IN_GGA(Z, Y)
REM_IN_GGA(y0, s(x0)) → U1_GGA(y0, s(x0), notZero_out_g)
U1_GGA(X, Y, notZero_out_g) → U2_GGA(Y, sub_in_gga(X, Y))
sub_in_gga(s(X), s(Y)) → U6_gga(sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X)
U6_gga(sub_out_gga(Z)) → sub_out_gga(Z)
sub_in_gga(x0, x1)
U6_gga(x0)
U1_GGA(s(x0), s(x1), notZero_out_g) → U2_GGA(s(x1), U6_gga(sub_in_gga(x0, x1)))
U1_GGA(x0, 0, notZero_out_g) → U2_GGA(0, sub_out_gga(x0))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
U2_GGA(Y, sub_out_gga(Z)) → REM_IN_GGA(Z, Y)
U1_GGA(s(x0), s(x1), notZero_out_g) → U2_GGA(s(x1), U6_gga(sub_in_gga(x0, x1)))
U1_GGA(x0, 0, notZero_out_g) → U2_GGA(0, sub_out_gga(x0))
REM_IN_GGA(y0, s(x0)) → U1_GGA(y0, s(x0), notZero_out_g)
sub_in_gga(s(X), s(Y)) → U6_gga(sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X)
U6_gga(sub_out_gga(Z)) → sub_out_gga(Z)
sub_in_gga(x0, x1)
U6_gga(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
U2_GGA(Y, sub_out_gga(Z)) → REM_IN_GGA(Z, Y)
U1_GGA(s(x0), s(x1), notZero_out_g) → U2_GGA(s(x1), U6_gga(sub_in_gga(x0, x1)))
REM_IN_GGA(y0, s(x0)) → U1_GGA(y0, s(x0), notZero_out_g)
sub_in_gga(s(X), s(Y)) → U6_gga(sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X)
U6_gga(sub_out_gga(Z)) → sub_out_gga(Z)
sub_in_gga(x0, x1)
U6_gga(x0)
U2_GGA(s(z1), sub_out_gga(x1)) → REM_IN_GGA(x1, s(z1))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ ForwardInstantiation
U1_GGA(s(x0), s(x1), notZero_out_g) → U2_GGA(s(x1), U6_gga(sub_in_gga(x0, x1)))
U2_GGA(s(z1), sub_out_gga(x1)) → REM_IN_GGA(x1, s(z1))
REM_IN_GGA(y0, s(x0)) → U1_GGA(y0, s(x0), notZero_out_g)
sub_in_gga(s(X), s(Y)) → U6_gga(sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X)
U6_gga(sub_out_gga(Z)) → sub_out_gga(Z)
sub_in_gga(x0, x1)
U6_gga(x0)
REM_IN_GGA(s(y_0), s(x1)) → U1_GGA(s(y_0), s(x1), notZero_out_g)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
U1_GGA(s(x0), s(x1), notZero_out_g) → U2_GGA(s(x1), U6_gga(sub_in_gga(x0, x1)))
U2_GGA(s(z1), sub_out_gga(x1)) → REM_IN_GGA(x1, s(z1))
REM_IN_GGA(s(y_0), s(x1)) → U1_GGA(s(y_0), s(x1), notZero_out_g)
sub_in_gga(s(X), s(Y)) → U6_gga(sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X)
U6_gga(sub_out_gga(Z)) → sub_out_gga(Z)
sub_in_gga(x0, x1)
U6_gga(x0)
U2_GGA(s(x0), sub_out_gga(s(y_0))) → REM_IN_GGA(s(y_0), s(x0))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ QDPOrderProof
U1_GGA(s(x0), s(x1), notZero_out_g) → U2_GGA(s(x1), U6_gga(sub_in_gga(x0, x1)))
U2_GGA(s(x0), sub_out_gga(s(y_0))) → REM_IN_GGA(s(y_0), s(x0))
REM_IN_GGA(s(y_0), s(x1)) → U1_GGA(s(y_0), s(x1), notZero_out_g)
sub_in_gga(s(X), s(Y)) → U6_gga(sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X)
U6_gga(sub_out_gga(Z)) → sub_out_gga(Z)
sub_in_gga(x0, x1)
U6_gga(x0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U2_GGA(s(x0), sub_out_gga(s(y_0))) → REM_IN_GGA(s(y_0), s(x0))
Used ordering: Polynomial interpretation [25]:
U1_GGA(s(x0), s(x1), notZero_out_g) → U2_GGA(s(x1), U6_gga(sub_in_gga(x0, x1)))
REM_IN_GGA(s(y_0), s(x1)) → U1_GGA(s(y_0), s(x1), notZero_out_g)
POL(0) = 0
POL(REM_IN_GGA(x1, x2)) = x1
POL(U1_GGA(x1, x2, x3)) = x1
POL(U2_GGA(x1, x2)) = x2
POL(U6_gga(x1)) = x1
POL(notZero_out_g) = 0
POL(s(x1)) = 1 + x1
POL(sub_in_gga(x1, x2)) = 1 + x1
POL(sub_out_gga(x1)) = 1 + x1
U6_gga(sub_out_gga(Z)) → sub_out_gga(Z)
sub_in_gga(X, 0) → sub_out_gga(X)
sub_in_gga(s(X), s(Y)) → U6_gga(sub_in_gga(X, Y))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
U1_GGA(s(x0), s(x1), notZero_out_g) → U2_GGA(s(x1), U6_gga(sub_in_gga(x0, x1)))
REM_IN_GGA(s(y_0), s(x1)) → U1_GGA(s(y_0), s(x1), notZero_out_g)
sub_in_gga(s(X), s(Y)) → U6_gga(sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X)
U6_gga(sub_out_gga(Z)) → sub_out_gga(Z)
sub_in_gga(x0, x1)
U6_gga(x0)